A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
(can-apply(f o g  ;x))  (do-apply(f o g  ;x) ~ do-apply(f;do-apply(g;x))) 

latex

ProofTree

Definitions

Type, f o g  , can-apply(f;x), do-apply(f;x), f(a), Top, s = t, x:A. B(x), x:AB(x), t  T, left + right, b, P  Q, False